Definition mynat := nat.
